Section: New Software and Platforms

CoqInterval

Interval package for Coq

Keywords: Interval arithmetic - Coq

Functional Description

CoqInterval is a library for the proof assistant Coq. CoqInterval provides a method for proving automatically the inequality of two expression of real values.

The Interval package provides several tactics for helping a Coq user to prove theorems on enclosures of real-valued expressions. The proofs are performed by an interval kernel which relies on a computable formalization of floating-point arithmetic in Coq.

The Marelle team developed a formalization of rigorous polynomial approximation using Taylor models inside the Coq proof assistant, with a special focus on genericity and efficiency for the computations. In 2014, this library has been included in CoqInterval.

• Participants: Guillaume Melquiond, Erik Martin Dorel, Nicolas Brisebarre, Miora Maria Joldes, Micaela Mayero, Jean Michel Muller, Laurence Rideau and Laurent Thery

• Contact: Guillaume Melquiond

• URL: http://coq-interval.gforge.inria.fr/